COMMENT ⊗   VALID 00003 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	.EVERY HEADING (Preliminary User's Manual , ,{DATE})
 00006 00003	VI. PRIMITIVE PATTERN LANGUAGE.
 00012 ENDMK
⊗;
.EVERY HEADING (Preliminary User's Manual , ,{DATE})

V. SEARCHING AND PATTERN MATCHING.

.BEGIN DOUBLE SPACE

The pattern matching facilities for interactive theorem proving
are the most difficult feature to describe well. The tools presented to the
user should be general enough to significantly aid in the search for a proof.
At the same time the pattern matching commands should be concise and somewhat
readable.
Clearly, pattern matching is present throughout the theorem prover; the
choice strategies, the rules of inference, and the editing strategies are all
examples of very sophisticated pattern matching. Thus pattern matching is
 very important part of the theorem proving process. Indeed we
are currently exploring a general theroem proving language which will exploit
pattern matching in all aspects of proof search -- rules, strategies, and heuristics.

Pattern matching is invoked by the FIND operation. FIND[<id>,<pattern>] expects
<id> to be the name of a list of clauses, and <pattern> should be a Boolean
combination of primitive patterns. These primitive patterns are completely described in the
next section, but basically allow description of syntactic parts of clauses.

Since many of the applications of FIND are of the form FIND[CLAUSES,<pattern>],
the abbreviation, FINDC[<pattern>] has been added for this case.

Here's an example of FIND and FINDC. 

.END
.BEGIN VERBATIM
SET XX FINDC[0εC];    	|C is a 'clauses variable'. The pattern says
			|find all clauses in the set CLAUSES which 
			|have occurrences of the symbol 0.
			|In this problem 0 is a function letter.
*
DI XX;			|Display the clauses.

1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
3 0≤x;
4 x/x=0;
5 x/1=0;
*

SET YY FIND[XX,≤εC];	|Find all clauses in XX which have occurrences
			|of the symbol '≤', and assign those clauses 
			|to YY.
*
DI YY;			|Display YY.
1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
*

SET ZZ FIND[YY,/εC∧=εC];
*
SET ZZ FIND[YY,⊂/,=⊃εC];|These  last two patterns have exactly the 
			|same effect.
*

.END
VI. PRIMITIVE PATTERN LANGUAGE.

.BEGIN DOUBLE SPACE
A simple language has been devised for more precise descriptions of 
strategies than Boolean combinations of the builtin strategies.
This language is also useful for describing patterns for searching clause
lists using FIND and FINDC.

This language allows rather arbitrary functions on the syntactic structure 
of clauses terms and literal.

The interpretation of the constructed formulas differs depending on whether
the formula is an editing strategy, a choice strategy, or a pattern.
Formulas  to be used for choice strategies are supposed to be applied
to a binary rule of inference, I, in the presence of two clauses, C1 and C2;
that is, I(C1,C2).
An editing strategy formula is to be applied to a single clause, thus there
should be exactly one `clause variable', currently named C.
Thus when we give choice strategies then formula is used as a filter on each
pair of candidates. 
When we use the formulas on clause-lists in the editing phase, they
ae to be applied to each clause, any clause satisfying the editing formula is
to be edited out.


PRIMITIVES:

1) ancestry	TR(x)

Examples:

If x is an initial clauses then TR(x) is NIL. If x is a deduction then TR gives
a  list of the clauses appearing in the derivation tree.

2) length		α(x)

If x is a clause then α(x) gives the usual length--number of literals.

Examples:

α(C1)=1 is true if C1 is a unit-clause.

3) depth		∂(x)

This gives the maximum depth of function nesting in the clause,x.
.END

.BEGIN VERBATIM

PREDICATES:

=,<,>,¬		equality,less-than,greater-than, not
∧,∨,ε		and,or,clever membership.
[ p→e; ...]	conditionals

.END

.BEGIN DOUBLE SPACE

Examples:
a) ∂(C1)<5 ∧TR(C1)=NIL

Depth of nesting is less than 5 and clause is initial.


MATCHING:

+,-		sign of a literal
⊂,⊃		set delimiters for and-membership
⊃,⊂		set delimiters for or-membershit

Examples;
⊂2,3,4⊃εTR(c)

   Each clause 2,3,and 4 must appear in the tree of c.

⊃2,3,4⊂εTR(c)

   At least one of these clauses must appeaar.

_		matches any term

x,y,z,u,v	used to match sub-terms.

Examples:
f(_,_) matches any occurrence of the function-letter,f.

f(g(x,_),_,x) matches any occurrence of f such that f's first position is
an occurrence of g; and g's first position matches the third position of f.

Examples:

Definition of some of the builtin strategies in the language.

.END

.BEGIN VERBATIM

ANCESTRY: 	TR(C1)=NIL ∨ TR(C2)=NIL ∨ C2εTR(C1) ∨ C1εTR(C2)
SUPPORT[...]:  	[TR(C2)=NIL → ⊃...⊂εTR(C2);T → T]
UNIT:  		α(C1)=1 ∨ α(C2)=1
VINE: 		TR(C1)=NIL ∨ TR(C2)=1

LENGTH[#]: 	α(C) > # 
DEPTH[#]: 	∂(C) > #

.END